(set-logic NRA)
(set-option :model_validate true)
(set-option :model true)
(set-option :unsat_core false)
(set-option :smt.arith.auto_config_simplex false)
(set-option :smt.arith.random_initial_value false)
(set-option :smt.arith.greatest_error_pivot true)
(set-option :smt.dack.eq true)
(set-option :smt.arith.int_eq_branch false)
(set-option :smt.core.extend_nonlocal_patterns true)
(set-option :smt.theory_case_split true)
(set-option :smt.theory_aware_branching true)
(set-option :model.inline_def false)
(set-option :model.partial false)
(set-option :nlsat.minimize_conflicts false)
;(set-option :nlsat.inline_vars true)
(set-option :nlsat.log_lemmas false)
(set-option :nlsat.reorder false)
(set-option :nlsat.factor true)
(set-option :nlsat.randomize false)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const r4 Real)
(declare-const r5 Real)
(declare-const r6 Real)
(declare-const r10 Real)
(declare-const r11 Real)
(declare-const r13 Real)
(declare-const v16 Bool)
(assert (or v11 v5))
(assert (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10))
(assert v0)
(assert v14)
(declare-const v17 Bool)
(assert (exists ((q0 Real) (q1 Bool) (q2 Bool)) v5))
(declare-const r14 Real)
(assert v14)
(assert (exists ((q3 Bool)) v17))
(assert v2)
(declare-const v18 Bool)
(declare-const v19 Bool)
(assert v1)
(declare-const v20 Bool)
(declare-const v21 Bool)
(assert v4)
(declare-const r15 Real)
(assert (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2))
(declare-const v22 Bool)
(assert (= v22 (= r11 r1 r5 r2) v15 v4))
(check-sat)
(declare-const v23 Bool)
(assert v13)
(assert v12)
(check-sat)
(declare-const v24 Bool)
(declare-const r16 Real)
(assert v10)
(declare-const v25 Bool)
(assert v6)
(declare-const r17 Real)
(assert (or (= r1 r1 4930 63967686 8024.32) v25 (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v11 (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329)))))
(declare-const v26 Bool)
(assert (forall ((q4 Bool) (q5 Bool) (q6 Bool)) v18))
(assert (xor (distinct v16 v0 v13) v0 (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v21 v26 (or v11 v5) (=> v1 v15)))
(assert (> r1 r6 8024.32 r11 349))
(assert (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24))
(declare-const r18 Real)
(assert (not v5))
(declare-const v27 Bool)
(declare-const v28 Bool)
(declare-const r19 Real)
(declare-const v29 Bool)
(declare-const v30 Bool)
(declare-const r20 Real)
(declare-const r21 Real)
(declare-const v31 Bool)
(assert (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6))
(declare-const v32 Bool)
(assert (exists ((q7 Bool) (q8 Bool) (q9 Bool) (q10 Bool)) (not (and q9 v26 v24 v22 (not v5) q10 v32 (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) (distinct v16 v0 v13) (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) q10))))
(assert (or v6 v5 v20 (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6)))
(assert (distinct v12 v31 (=> v3 v14) (distinct 86 349) (=> (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v2) v10 v25 (not v20) v27 (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24)))
(push 1)
(declare-const v33 Bool)
(assert v12)
(declare-const r22 Real)
(assert (xor (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v33 v0 (= r0 6214429792) v15 (distinct (=> v1 v15) v6 v0 (or v11 v5) v9 (distinct r11 r14 4930 r6)) v17 (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24)))
(assert (distinct (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (=> (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v2) v4 (not v5) v29 v33))
(declare-const v34 Bool)
(declare-const v35 Bool)
(assert (= (not v5) v30 (or (= r1 r1 4930 63967686 8024.32) v25 (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v11 (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329)))) v16 (> r0 396104441 (- (* 396104441 r4)) 63967686 (- 991360138)) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v35))
(pop 1)
(assert (=> v15 v17))
(declare-const v36 Bool)
(assert (=> (> (* 396104441 r4) r5 r2 r13 86) (xor (distinct v16 v0 v13) v0 (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v21 v26 (or v11 v5) (=> v1 v15))))
(declare-const v37 Bool)
(assert (distinct (= v22 (= r11 r1 r5 r2) v15 v4) v0 (> r1 r6 8024.32 r11 349) (not v7) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v22 v20 (=> (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v2) (or v6 v5 v20 (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6)) v9))
(push 1)
(assert (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)))
(declare-const r23 Real)
(assert (or (xor v3 v24 (= r10 (/ r1 0.449680329))) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v23))
(declare-const v38 Bool)
(declare-const r24 Real)
(declare-const r25 Real)
(assert (distinct v17 (xor v3 v24 (= r10 (/ r1 0.449680329))) (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) v18 (> r1 r6 8024.32 r11 349) (=> v3 v14) v9 v16 (=> v1 v15) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329)))))
(declare-const v39 Bool)
(declare-const v40 Bool)
(declare-const v41 Bool)
(assert (xor (xor v13 v2 v6 v10 v19 v11 v2) (> r1 r6 8024.32 r11 349) (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (>= r6 6214429792 (- (/ r1 0.449680329)) 63967686) (> 86 (* 86 (/ r1 0.449680329)) r0 (/ r1 0.449680329)) v37 (xor (distinct v5 v3 v10 v22 (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24) (= r11 r1 r5 r2) (= r10 (/ r1 0.449680329))) (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v8 (= r10 (/ r1 0.449680329)) (not v20) (not v20) (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (> 8024.32 (+ r6 991360138) (/ 0.4490045 8024.32))) v19 (not v7) (= 4930 r11 27376593588 0.370148902 63967686) v24))
(declare-const v42 Bool)
(assert (>= r13 (* 396104441 r4) 0.4490045 r17))
(declare-const v43 Bool)
(declare-const r26 Real)
(declare-const v44 Bool)
(assert (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))))
(declare-const v45 Bool)
(assert (forall ((q11 Real) (q12 Real) (q13 Real)) (not (distinct q11 q12 q11 q13))))
(push 1)
(assert (or (= r1 r1 4930 63967686 8024.32) v25 (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v11 (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329)))))
(assert v29)
(push 1)
(pop 1)
(assert (distinct v42 v40 v32 (or (not v6) (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10) v19 v13) v23 (or (not v6) (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10) v19 v13) (= r11 r1 r5 r2) v44 v12 v19))
(check-sat)
(assert (=> v1 v32))
(assert (<= 0.370148902 r23 6985.793 r20 (* 396104441 r4)))
(declare-const v46 Bool)
(assert (xor (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) (xor (distinct v16 v0 v13) v0 (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v21 v26 (or v11 v5) (=> v1 v15)) (xor (distinct v5 v3 v10 v22 (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24) (= r11 r1 r5 r2) (= r10 (/ r1 0.449680329))) (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v8 (= r10 (/ r1 0.449680329)) (not v20) (not v20) (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (> 8024.32 (+ r6 991360138) (/ 0.4490045 8024.32))) (xor v13 v2 v6 v10 v19 v11 v2) v8 v36 (distinct r11 r14 4930 r6) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v10 v30 (> 349 86)))
(declare-const r27 Real)
(assert (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)))
(check-sat)
(declare-const v47 Bool)
(assert v47)
(assert (distinct (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10) v15 (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10) (distinct r11 r14 4930 r6) v15 (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (distinct r11 r14 4930 r6) (distinct (- r4) 86 0.28753)))
(declare-const r28 Real)
(declare-const v48 Bool)
(assert (distinct v42 (= r11 r1 r5 r2) (not v6)))
(push 1)
(assert v6)
(assert (not (or (or (= r1 r1 4930 63967686 8024.32) v25 (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v11 (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329)))) (xor (distinct v16 v0 v13) v0 (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v21 v26 (or v11 v5) (=> v1 v15)) v3 v22 v13 (xor v13 v2 v6 v10 v19 v11 v2) (> 86 (* 86 (/ r1 0.449680329)) r0 (/ r1 0.449680329)) (> 86 (* 86 (/ r1 0.449680329)) r0 (/ r1 0.449680329)) (distinct v12 v31 (=> v3 v14) (distinct 86 349) (=> (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v2) v10 v25 (not v20) v27 (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24)) v16)))
(pop 1)
(assert v22)
(declare-const r29 Real)
(assert (and v1 v30 (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (= 4930 r11 27376593588 0.370148902 63967686) (or v11 v5) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v21 v37 v0))
(declare-const r30 Real)
(push 1)
(pop 1)
(assert (= v36 (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10) (= v2 (distinct v5 v3 v10 v22 (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24) (= r11 r1 r5 r2) (= r10 (/ r1 0.449680329))) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v20 v23 v18 (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v2) v26 (= r1 r1 4930 63967686 8024.32) v31 (not v7) v39))
(assert (not v5))
(declare-const v49 Bool)
(push 1)
(declare-const v50 Bool)
(assert v25)
(declare-const v51 Bool)
(assert v48)
(check-sat)
(push 1)
(declare-const v52 Bool)
(assert (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)))
(push 1)
(declare-const v53 Bool)
(assert (forall ((q14 Bool) (q15 Real) (q16 Bool)) v51))
(declare-const v54 Bool)
(declare-const r31 Real)
(declare-const v55 Bool)
(assert (xor (xor v13 v2 v6 v10 v19 v11 v2) (> r1 r6 8024.32 r11 349) (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (>= r6 6214429792 (- (/ r1 0.449680329)) 63967686) (> 86 (* 86 (/ r1 0.449680329)) r0 (/ r1 0.449680329)) v37 (xor (distinct v5 v3 v10 v22 (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24) (= r11 r1 r5 r2) (= r10 (/ r1 0.449680329))) (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v8 (= r10 (/ r1 0.449680329)) (not v20) (not v20) (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (> 8024.32 (+ r6 991360138) (/ 0.4490045 8024.32))) v19 (not v7) (= 4930 r11 27376593588 0.370148902 63967686) v24))
(assert v38)
(push 1)
(push 1)
(declare-const v56 Bool)
(assert (=> v15 v17))
(push 1)
(declare-const v57 Bool)
(pop 1)
(declare-const v58 Bool)
(assert (exists ((q17 Bool) (q18 Real) (q19 Real) (q20 Real)) (=> (= (xor (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) (xor (distinct v16 v0 v13) v0 (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v21 v26 (or v11 v5) (=> v1 v15)) (xor (distinct v5 v3 v10 v22 (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24) (= r11 r1 r5 r2) (= r10 (/ r1 0.449680329))) (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v8 (= r10 (/ r1 0.449680329)) (not v20) (not v20) (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (> 8024.32 (+ r6 991360138) (/ 0.4490045 8024.32))) (xor v13 v2 v6 v10 v19 v11 v2) v8 v36 (distinct r11 r14 4930 r6) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v10 v30 (> 349 86)) (not v5) q17) (< 97.41194 q20 q18 q19 q20))))
(declare-const v59 Bool)
(declare-const r32 Real)
(declare-const v60 Bool)
(assert (exists ((q21 Bool) (q22 Bool) (q23 Real) (q24 Bool)) (not (< q23 r21 74329677 q23))))
(push 1)
(assert (forall ((q25 Real) (q26 Bool) (q27 Real) (q28 Real)) (not (xor q26 q26 q26 q26))))
(declare-const r33 Real)
(declare-const r34 Real)
(assert (exists ((q29 Real)) (<= r17 1469428369)))
(assert (=> (>= 4930 r24) (= v36 (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10) (= v2 (distinct v5 v3 v10 v22 (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24) (= r11 r1 r5 r2) (= r10 (/ r1 0.449680329))) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v20 v23 v18 (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v2) v26 (= r1 r1 4930 63967686 8024.32) v31 (not v7) v39)))
(pop 1)
(declare-const v61 Bool)
(assert (>= r6 6214429792 (- (/ r1 0.449680329)) 63967686))
(declare-const v62 Bool)
(assert (or v9 (= r10 (/ r1 0.449680329)) (or (xor v3 v24 (= r10 (/ r1 0.449680329))) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v23) (>= r6 6214429792 (- (/ r1 0.449680329)) 63967686) (< 1469428369 4930 2 8024.32 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (>= 0.370148902 (- (+ r6 991360138)) (/ r21 (/ r1 0.449680329))) (> r1 r6 8024.32 r11 349) v40))
(check-sat)
(declare-const v63 Bool)
(assert (and (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10) v29 (not v37) (= r11 r1 r5 r2) (distinct (> r1 r6 8024.32 r11 349) (= v22 (= r11 r1 r5 r2) v15 v4) (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10) (distinct v12 v31 (=> v3 v14) (distinct 86 349) (=> (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v2) v10 v25 (not v20) v27 (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24)) (distinct v16 v0 v13) (not v6) v1)))
(check-sat)
(declare-const v64 Bool)
(declare-const r35 Real)
(push 1)
(declare-const r36 Real)
(declare-const v65 Bool)
(assert (or v6 v5 v20 (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6)))
(assert (or (distinct (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32)) r32 (/ (+ r1 r16 0.449680329 0.449680329 (+ r6 991360138)) 396104441) (* 0.449680329 0.449680329 (+ 991360138 349) (/ (* r14 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32)) r2 r5 63967686) r4)) r31) (= (/ (- (/ (/ r1 0.449680329) r18)) 2) 97.41194 (/ (+ r1 r16 0.449680329 0.449680329 (+ r6 991360138)) (- r17)) r30) (=> v1 v32) v49 v2 (=> (> (* 396104441 r4) r5 r2 r13 86) (xor (distinct v16 v0 v13) v0 (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v21 v26 (or v11 v5) (=> v1 v15))) (not (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10))))
(declare-const v66 Bool)
(assert v30)
(assert (not v51))
(declare-const r37 Real)
(assert (xor (=> v15 v17) v46 (> 8024.32 (+ r6 991360138) (/ 0.4490045 8024.32))))
(declare-const v67 Bool)
(assert v51)
(check-sat)
(assert (forall ((q30 Real) (q31 Real) (q32 Real)) (not (< q32 q30 (- r23)))))
(declare-const v68 Bool)
(declare-const r38 Real)
(assert (= r1 r1 4930 63967686 8024.32))
(declare-const v69 Bool)
(declare-const r39 Real)
(declare-const v70 Bool)
(assert (exists ((q33 Real) (q34 Real) (q35 Bool) (q36 Bool)) (or v11 v5)))
(declare-const v71 Bool)
(pop 1)
(declare-const v72 Bool)
(declare-const v73 Bool)
(assert (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2))
(declare-const v74 Bool)
(assert v1)
(declare-const v75 Bool)
(declare-const r40 Real)
(assert (or (= (- 86) (/ 0.4490045 8024.32) 86 r19 74329677) v26 v36 (< 2 (- r16 r24 r13 (/ r21 (/ r1 0.449680329))) 349 97.41194) v15 (< (- r16) (- (* 396104441 r4)) 1558551011)))
(pop 1)
(assert v38)
(assert (or v10 (xor (= r1 r1 4930 63967686 8024.32) v45 v52 (xor (xor (xor v13 v2 v6 v10 v19 v11 v2) (> r1 r6 8024.32 r11 349) (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (>= r6 6214429792 (- (/ r1 0.449680329)) 63967686) (> 86 (* 86 (/ r1 0.449680329)) r0 (/ r1 0.449680329)) v37 (xor (distinct v5 v3 v10 v22 (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24) (= r11 r1 r5 r2) (= r10 (/ r1 0.449680329))) (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v8 (= r10 (/ r1 0.449680329)) (not v20) (not v20) (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (> 8024.32 (+ r6 991360138) (/ 0.4490045 8024.32))) v19 (not v7) (= 4930 r11 27376593588 0.370148902 63967686) v24) (distinct (> r1 r6 8024.32 r11 349) (= v22 (= r11 r1 r5 r2) v15 v4) (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10) (distinct v12 v31 (=> v3 v14) (distinct 86 349) (=> (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v2) v10 v25 (not v20) v27 (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24)) (distinct v16 v0 v13) (not v6) v1) (not (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10)) (> 8024.32 (+ r6 991360138) (/ 0.4490045 8024.32))) v12 (> 349 86) v38 v52 (not (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10)) v0 v43) (xor v40 v21 (distinct v17 (xor v3 v24 (= r10 (/ r1 0.449680329))) (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) v18 (> r1 r6 8024.32 r11 349) (=> v3 v14) v9 v16 (=> v1 v15) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329)))) (= 4930 r11 27376593588 0.370148902 63967686) v30 (>= 4930 r24) (> (* 396104441 r4) r5 r2 r13 86) (or v6 v5 v20 (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6)) (=> (> (* 396104441 r4) r5 r2 r13 86) (xor (distinct v16 v0 v13) v0 (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v21 v26 (or v11 v5) (=> v1 v15)))) (xor v40 v21 (distinct v17 (xor v3 v24 (= r10 (/ r1 0.449680329))) (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) v18 (> r1 r6 8024.32 r11 349) (=> v3 v14) v9 v16 (=> v1 v15) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329)))) (= 4930 r11 27376593588 0.370148902 63967686) v30 (>= 4930 r24) (> (* 396104441 r4) r5 r2 r13 86) (or v6 v5 v20 (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6)) (=> (> (* 396104441 r4) r5 r2 r13 86) (xor (distinct v16 v0 v13) v0 (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v21 v26 (or v11 v5) (=> v1 v15)))) (not v5) (distinct v17 (xor v3 v24 (= r10 (/ r1 0.449680329))) (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) v18 (> r1 r6 8024.32 r11 349) (=> v3 v14) v9 v16 (=> v1 v15) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329)))) (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5))))
(declare-const v76 Bool)
(assert v22)
(declare-const v77 Bool)
(assert (=> v3 (=> (> (* 396104441 r4) r5 r2 r13 86) (xor (distinct v16 v0 v13) v0 (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v21 v26 (or v11 v5) (=> v1 v15)))))
(assert (not (or (xor v3 v24 (= r10 (/ r1 0.449680329))) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329))) v23)))
(assert (xor v44 (>= 4930 r24) (> 0.28753 r6 r26 r14 8.02674212) v22 (xor v40 v21 (distinct v17 (xor v3 v24 (= r10 (/ r1 0.449680329))) (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) v18 (> r1 r6 8024.32 r11 349) (=> v3 v14) v9 v16 (=> v1 v15) (distinct v22 v17 v18 v22 (= r1 r1 4930 63967686 8024.32) (= r10 (/ r1 0.449680329)))) (= 4930 r11 27376593588 0.370148902 63967686) v30 (>= 4930 r24) (> (* 396104441 r4) r5 r2 r13 86) (or v6 v5 v20 (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6)) (=> (> (* 396104441 r4) r5 r2 r13 86) (xor (distinct v16 v0 v13) v0 (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) v21 v26 (or v11 v5) (=> v1 v15)))) (xor (= r1 r1 4930 63967686 8024.32) v45 v52 (xor (xor (xor v13 v2 v6 v10 v19 v11 v2) (> r1 r6 8024.32 r11 349) (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (>= r6 6214429792 (- (/ r1 0.449680329)) 63967686) (> 86 (* 86 (/ r1 0.449680329)) r0 (/ r1 0.449680329)) v37 (xor (distinct v5 v3 v10 v22 (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24) (= r11 r1 r5 r2) (= r10 (/ r1 0.449680329))) (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v8 (= r10 (/ r1 0.449680329)) (not v20) (not v20) (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (> 8024.32 (+ r6 991360138) (/ 0.4490045 8024.32))) v19 (not v7) (= 4930 r11 27376593588 0.370148902 63967686) v24) (distinct (> r1 r6 8024.32 r11 349) (= v22 (= r11 r1 r5 r2) v15 v4) (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10) (distinct v12 v31 (=> v3 v14) (distinct 86 349) (=> (xor (distinct r11 r14 4930 r6) (not v7) v24 v10 v6) v2) v10 v25 (not v20) v27 (= v9 (xor (xor v13 v2 v6 v10 v19 v11 v2) v2 v0 v5 v17 v2) v7 v16 (not v5) (> r1 r6 8024.32 r11 349)) (and v1 (xor (xor v13 v2 v6 v10 v19 v11 v2) v10 (or v11 v5)) (=> v3 v14) v0 (= r1 r1 4930 63967686 8024.32) (> 0.4490045 (- (/ 0.4490045 8024.32) r1 (/ 0.4490045 8024.32))) (not v20) v19 v16 v20 v24)) (distinct v16 v0 v13) (not v6) v1) (not (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10)) (> 8024.32 (+ r6 991360138) (/ 0.4490045 8024.32))) v12 (> 349 86) v38 v52 (not (or v2 v3 v2 v8 v2 v11 v12 v7 v1 v9 v10)) v0 v43)))
;(check-sat-using (then simplify nlsat))
(exit)
